$\forall$$T$:Type, $R$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$).
\\[0ex]WellFnd\{i\}($T$;$x$,$y$.$R$($x$,$y$))
\\[0ex]$\Rightarrow$ ($\forall$$x$, $y$:$T$. Dec($R$($x$,$y$)))
\\[0ex]$\Rightarrow$ ($\forall$$y$:$T$. $\exists$$L$:$T$ List. ($\forall$$x$:$T$. ($R$($x$,$y$)) $\Rightarrow$ ($x$ $\in$ $L$)))
\\[0ex]$\Rightarrow$ ($\forall$$y$:$T$. $\exists$$x$:$T$. (($R$$^{\mbox{\scriptsize $\ast$}}$)($x$,$y$) \& ($\forall$$z$:$T$. $\neg$($R$($z$,$x$)))))